/-
Copyright (c) 2019 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Johan Commelin
-/
import group_theory.free_abelian_group

/-!
# Free rings

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

The theory of the free ring over a type.

## Main definitions

* `free_ring α` : the free (not commutative in general) ring over a type.
* `lift (f : α → R)` : the ring hom `free_ring α →+* R` induced by `f`.
* `map (f : α → β)` : the ring hom `free_ring α →+* free_ring β` induced by `f`.

## Implementation details

`free_ring α` is implemented as the free abelian group over the free monoid on `α`.

## Tags

free ring

-/

universes u v

/-- The free ring over a type `α`. -/
@[derive [ring, inhabited]]
def free_ring (α : Type u) : Type u :=
free_abelian_group $ free_monoid α

namespace free_ring

variables {α : Type u}

/-- The canonical map from α to `free_ring α`. -/
def of (x : α) : free_ring α :=
free_abelian_group.of (free_monoid.of x)

lemma of_injective : function.injective (of : α → free_ring α) :=
free_abelian_group.of_injective.comp free_monoid.of_injective

@[elab_as_eliminator] protected lemma induction_on
  {C : free_ring α → Prop} (z : free_ring α)
  (hn1 : C (-1)) (hb : ∀ b, C (of b))
  (ha : ∀ x y, C x → C y → C (x + y))
  (hm : ∀ x y, C x → C y → C (x * y)) : C z :=
have hn : ∀ x, C x → C (-x), from λ x ih, neg_one_mul x ▸ hm _ _ hn1 ih,
have h1 : C 1, from neg_neg (1 : free_ring α) ▸ hn _ hn1,
free_abelian_group.induction_on z
  (add_left_neg (1 : free_ring α) ▸ ha _ _ hn1 h1)
  (λ m, list.rec_on m h1 $ λ a m ih, hm _ _ (hb a) ih)
  (λ m ih, hn _ ih)
  ha

section lift

variables {R : Type v} [ring R] (f : α → R)

/-- The ring homomorphism `free_ring α →+* R` induced from a map `α → R`. -/
def lift : (α → R) ≃ (free_ring α →+* R) :=
free_monoid.lift.trans free_abelian_group.lift_monoid

@[simp] lemma lift_of (x : α) : lift f (of x) = f x :=
congr_fun (lift.left_inv f) x

@[simp] lemma lift_comp_of (f : free_ring α →+* R) : lift (f ∘ of) = f :=
lift.right_inv f

@[ext]
lemma hom_ext ⦃f g : free_ring α →+* R⦄ (h : ∀ x, f (of x) = g (of x)) :
  f = g :=
lift.symm.injective (funext h)

end lift

variables {β : Type v} (f : α → β)

/-- The canonical ring homomorphism `free_ring α →+* free_ring β` generated by a map `α → β`. -/
def map : free_ring α →+* free_ring β :=
lift $ of ∘ f

@[simp]
lemma map_of (x : α) : map f (of x) = of (f x) := lift_of _ _

end free_ring
